Termination w.r.t. Q proof of /tmp/tmpUCWDyx/ex13.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

PLUS₂(plus₂(n, m), u) -> PLUS₂(n, plus₂(m, u))
COND₄(true, x, y, z) -> PLUS₂(s₁(y), z)
PLUS₂(plus₂(n, m), u) -> PLUS₂(m, u)
COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)
DIV₂(x, s₁(y)) -> D₃(x, s₁(y), 0)
D₃(x, s₁(y), z) -> GE₂(x, z)
PLUS₂(n, s₁(m)) -> PLUS₂(n, m)
GE₂(s₁(u), s₁(v)) -> GE₂(u, v)

The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

PLUS₂(plus₂(n, m), u) -> PLUS₂(n, plus₂(m, u))
COND₄(true, x, y, z) -> PLUS₂(s₁(y), z)
PLUS₂(plus₂(n, m), u) -> PLUS₂(m, u)
COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)
DIV₂(x, s₁(y)) -> D₃(x, s₁(y), 0)
D₃(x, s₁(y), z) -> GE₂(x, z)
PLUS₂(n, s₁(m)) -> PLUS₂(n, m)
GE₂(s₁(u), s₁(v)) -> GE₂(u, v)

The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 3 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS₂(plus₂(n, m), u) -> PLUS₂(n, plus₂(m, u))
PLUS₂(plus₂(n, m), u) -> PLUS₂(m, u)
PLUS₂(n, s₁(m)) -> PLUS₂(n, m)

The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [13] we can delete all non-usable rules [14] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS₂(plus₂(n, m), u) -> PLUS₂(n, plus₂(m, u))
PLUS₂(plus₂(n, m), u) -> PLUS₂(m, u)
PLUS₂(n, s₁(m)) -> PLUS₂(n, m)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS₂(plus₂(n, m), u) -> PLUS₂(n, plus₂(m, u))
PLUS₂(plus₂(n, m), u) -> PLUS₂(m, u)
PLUS₂(n, s₁(m)) -> PLUS₂(n, m)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

plus₂(x0, s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [16] together with the size-change analysis [27] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PLUS₂(n, s₁(m)) -> PLUS₂(n, m)
The graph contains the following edges 1 >= 1, 2 > 2
PLUS₂(plus₂(n, m), u) -> PLUS₂(m, u)
The graph contains the following edges 1 > 1, 2 >= 2
PLUS₂(plus₂(n, m), u) -> PLUS₂(n, plus₂(m, u))
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(s₁(u), s₁(v)) -> GE₂(u, v)

The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(s₁(u), s₁(v)) -> GE₂(u, v)

R is empty.
The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(s₁(u), s₁(v)) -> GE₂(u, v)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [16] together with the size-change analysis [27] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GE₂(s₁(u), s₁(v)) -> GE₂(u, v)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)

The TRS R consists of the following rules:

div₂(x, s₁(y)) -> d₃(x, s₁(y), 0)
d₃(x, s₁(y), z) -> cond₄(ge₂(x, z), x, y, z)
cond₄(true, x, y, z) -> s₁(d₃(x, s₁(y), plus₂(s₁(y), z)))
cond₄(false, x, y, z) -> 0
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)
plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

d₃(x0, s₁(x1), x2)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z) at position [0] we obtained the following new rules:

D₃(x0, s₁(y1), 0) -> COND₄(true, x0, y1, 0)
D₃(0, s₁(y1), s₁(x0)) -> COND₄(false, 0, y1, s₁(x0))
D₃(s₁(x0), s₁(y1), s₁(x1)) -> COND₄(ge₂(x0, x1), s₁(x0), y1, s₁(x1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D₃(s₁(x0), s₁(y1), s₁(x1)) -> COND₄(ge₂(x0, x1), s₁(x0), y1, s₁(x1))
COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x0, s₁(y1), 0) -> COND₄(true, x0, y1, 0)
D₃(0, s₁(y1), s₁(x0)) -> COND₄(false, 0, y1, s₁(x0))

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D₃(s₁(x0), s₁(y1), s₁(x1)) -> COND₄(ge₂(x0, x1), s₁(x0), y1, s₁(x1))
COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x0, s₁(y1), 0) -> COND₄(true, x0, y1, 0)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z)) at position [2] we obtained the following new rules:

COND₄(true, y0, y1, s₁(x1)) -> D₃(y0, s₁(y1), s₁(plus₂(s₁(y1), x1)))
COND₄(true, y0, y1, 0) -> D₃(y0, s₁(y1), s₁(y1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ DependencyGraphProof

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, y0, y1, s₁(x1)) -> D₃(y0, s₁(y1), s₁(plus₂(s₁(y1), x1)))
COND₄(true, y0, y1, 0) -> D₃(y0, s₁(y1), s₁(y1))
D₃(s₁(x0), s₁(y1), s₁(x1)) -> COND₄(ge₂(x0, x1), s₁(x0), y1, s₁(x1))
D₃(x0, s₁(y1), 0) -> COND₄(true, x0, y1, 0)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ QDP

                                    ↳ Instantiation

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, y0, y1, s₁(x1)) -> D₃(y0, s₁(y1), s₁(plus₂(s₁(y1), x1)))
D₃(s₁(x0), s₁(y1), s₁(x1)) -> COND₄(ge₂(x0, x1), s₁(x0), y1, s₁(x1))

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule COND₄(true, y0, y1, s₁(x1)) -> D₃(y0, s₁(y1), s₁(plus₂(s₁(y1), x1))) we obtained the following new rules:

COND₄(true, s₁(z0), z1, s₁(z2)) -> D₃(s₁(z0), s₁(z1), s₁(plus₂(s₁(z1), z2)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ QDP

                                    ↳ Instantiation

                                      ↳ QDP

            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, s₁(z0), z1, s₁(z2)) -> D₃(s₁(z0), s₁(z1), s₁(plus₂(s₁(z1), z2)))
D₃(s₁(x0), s₁(y1), s₁(x1)) -> COND₄(ge₂(x0, x1), s₁(x0), y1, s₁(x1))

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
d₃(x0, s₁(x1), x2)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

d₃(x0, s₁(x1), x2)
cond₄(false, x0, x1, x2)
cond₄(true, x0, x1, x2)
div₂(x0, s₁(x1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

COND₄(true, x, y, z) -> D₃(x, s₁(y), plus₂(s₁(y), z))
D₃(x, s₁(y), z) -> COND₄(ge₂(x, z), x, y, z)

The TRS R consists of the following rules:

plus₂(n, 0) -> n
plus₂(n, s₁(m)) -> s₁(plus₂(n, m))
plus₂(plus₂(n, m), u) -> plus₂(n, plus₂(m, u))
ge₂(u, 0) -> true
ge₂(0, s₁(v)) -> false
ge₂(s₁(u), s₁(v)) -> ge₂(u, v)

The set Q consists of the following terms:

ge₂(x0, 0)
plus₂(x0, s₁(x1))
ge₂(0, s₁(x0))
ge₂(s₁(x0), s₁(x1))
plus₂(x0, 0)
plus₂(plus₂(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.